es-responsive(es;l1;tg1;l2;tg2)
== (e=rcv(l1,tg1).
== (e'=rcv(l2,tg2).
== (e  sender(e') 
== (& (e2=rcv(l1,tg1). (e <loc e2)  (sender(e') <loc e2))
== (& (e''=rcv(l2,tg2). sender(e'') = sender(e')  e'' = e'))
== & (e'=rcv(l2,tg2).
== & (e=rcv(l1,tg1).
== & (e  sender(e') 
== & (& (e''=rcv(l2,tg2). (sender(e'') <loc sender(e'))  (sender(e'') <loc e))) 

latex

---

clarification:

es-responsive(es;l1;tg1;l2;tg2)
== alle-rcv(es;l1;tg1;e.existse-rcv(es;l2;tg2;e'.es-le(es;e;es-sender(es; e'))
== & alle-rcv(es;l1;tg1;e2.es-locl(es; e; e2)  es-locl(es; es-sender(es; e'); e2))
== & alle-rcv(es;l2;tg2;e''.es-sender(es; e'') = es-sender(es; e')  es-E(es)
== & alle-rcv(es;l2;tg2;e''. e'' = e'  es-E(es))))
== & alle-rcv(es;l2;tg2;e'.existse-rcv(es;l1;tg1;e.es-le(es;e;es-sender(es; e'))
== & & alle-rcv(es;l2;tg2;e''.es-locl(es; es-sender(es; e''); es-sender(es; e'))
== & & alle-rcv(es;l2;tg2;e''. es-locl(es; es-sender(es; e''); e)))) 

latex

Definitions	s = t, E, e=rcv(l,tg). P(e), P & Q, e  e' , e=rcv(l,tg). P(e), P  Q, (e <loc e'), sender(e)
FDL editor aliases	es-responsive